G2C: Cryptographic Protocols from Goal-Driven Specifications
Identifieur interne : 000283 ( Main/Exploration ); précédent : 000282; suivant : 000284G2C: Cryptographic Protocols from Goal-Driven Specifications
Auteurs : Michael Backes [Allemagne] ; Matteo Maffei [Allemagne] ; Kim Pecina [Allemagne] ; M. Reischuk [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2012.
Abstract
Abstract: We present G2C, a goal-driven specification language for distributed applications. This language offers support for the declarative specification of functionality goals and security properties. The former comprise the parties, their inputs, and the goal of the communication protocol. The latter comprise secrecy, access control, and anonymity requirements. A key feature of our language is that it abstracts away from how the intended functionality is achieved, but instead lets the system designer concentrate on which functional features and security properties should be achieved. Our framework provides a compilation method for transforming G2C specifications into symbolic cryptographic protocols, which are shown to be optimal. We provide a technique to automatically verify the correctness and security of these protocols using ProVerif, a state-of-the-art automated theorem-prover for cryptographic protocols. We have implemented a G2C compiler to demonstrate the feasibility of our approach.
Url:
DOI: 10.1007/978-3-642-27375-9_4
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000E35
- to stream Istex, to step Curation: 000E02
- to stream Istex, to step Checkpoint: 000018
- to stream Main, to step Merge: 000286
- to stream Main, to step Curation: 000283
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">G2C: Cryptographic Protocols from Goal-Driven Specifications</title><author><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name></author><author><name sortKey="Maffei, Matteo" sort="Maffei, Matteo" uniqKey="Maffei M" first="Matteo" last="Maffei">Matteo Maffei</name></author><author><name sortKey="Pecina, Kim" sort="Pecina, Kim" uniqKey="Pecina K" first="Kim" last="Pecina">Kim Pecina</name></author><author><name sortKey="Reischuk, M" sort="Reischuk, M" uniqKey="Reischuk M" first="M." last="Reischuk">M. Reischuk</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5C5F8A25FE2FA39F2E9600F403B9D1567461A64D</idno><date when="2012" year="2012">2012</date><idno type="doi">10.1007/978-3-642-27375-9_4</idno><idno type="url">https://api.istex.fr/document/5C5F8A25FE2FA39F2E9600F403B9D1567461A64D/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000E35</idno><idno type="wicri:Area/Istex/Curation">000E02</idno><idno type="wicri:Area/Istex/Checkpoint">000018</idno><idno type="wicri:doubleKey">0302-9743:2012:Backes M:g:c:cryptographic</idno><idno type="wicri:Area/Main/Merge">000286</idno><idno type="wicri:Area/Main/Curation">000283</idno><idno type="wicri:Area/Main/Exploration">000283</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">G2C: Cryptographic Protocols from Goal-Driven Specifications</title><author><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Saarland University, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max Planck Institute for Software Systems (MPI-SWS)</wicri:regionArea></affiliation></author><author><name sortKey="Maffei, Matteo" sort="Maffei, Matteo" uniqKey="Maffei M" first="Matteo" last="Maffei">Matteo Maffei</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Saarland University, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author><author><name sortKey="Pecina, Kim" sort="Pecina, Kim" uniqKey="Pecina K" first="Kim" last="Pecina">Kim Pecina</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Saarland University, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author><author><name sortKey="Reischuk, M" sort="Reischuk, M" uniqKey="Reischuk M" first="M." last="Reischuk">M. Reischuk</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Saarland University, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2012</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">5C5F8A25FE2FA39F2E9600F403B9D1567461A64D</idno><idno type="DOI">10.1007/978-3-642-27375-9_4</idno><idno type="ChapterID">4</idno><idno type="ChapterID">Chap4</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present G2C, a goal-driven specification language for distributed applications. This language offers support for the declarative specification of functionality goals and security properties. The former comprise the parties, their inputs, and the goal of the communication protocol. The latter comprise secrecy, access control, and anonymity requirements. A key feature of our language is that it abstracts away from how the intended functionality is achieved, but instead lets the system designer concentrate on which functional features and security properties should be achieved. Our framework provides a compilation method for transforming G2C specifications into symbolic cryptographic protocols, which are shown to be optimal. We provide a technique to automatically verify the correctness and security of these protocols using ProVerif, a state-of-the-art automated theorem-prover for cryptographic protocols. We have implemented a G2C compiler to demonstrate the feasibility of our approach.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Sarre (Land)</li></region><settlement><li>Sarrebruck</li></settlement></list><tree><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name></region><name sortKey="Backes, Michael" sort="Backes, Michael" uniqKey="Backes M" first="Michael" last="Backes">Michael Backes</name><name sortKey="Maffei, Matteo" sort="Maffei, Matteo" uniqKey="Maffei M" first="Matteo" last="Maffei">Matteo Maffei</name><name sortKey="Pecina, Kim" sort="Pecina, Kim" uniqKey="Pecina K" first="Kim" last="Pecina">Kim Pecina</name><name sortKey="Reischuk, M" sort="Reischuk, M" uniqKey="Reischuk M" first="M." last="Reischuk">M. Reischuk</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Ticri/CIDE/explor/OcrV1/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000283 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000283 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Ticri/CIDE
|area= OcrV1
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:5C5F8A25FE2FA39F2E9600F403B9D1567461A64D
|texte= G2C: Cryptographic Protocols from Goal-Driven Specifications
}}
| This area was generated with Dilib version V0.6.32. |  |